/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

#pragma once

#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif /* HAVE_AUTOCONF */
/*Z seL4内核对象类型 */
typedef enum _object {
    seL4_X86_4K = seL4_ModeObjectTypeCount, /*Z 4K页 */
    seL4_X86_LargePageObject,               /*Z 大页 */
    seL4_X86_PageTableObject,               /*Z 四级页表 */
    seL4_X86_PageDirectoryObject,           /*Z 三级页表 */
#ifdef CONFIG_IOMMU
    seL4_X86_IOPageTableObject,             /*Z IO页表 */
#endif
#ifdef CONFIG_VTX
    seL4_X86_VCPUObject,                    /*Z VCPU */
    seL4_X86_EPTPML4Object,                 /*Z EPT一级页表 */
    seL4_X86_EPTPDPTObject,                 /*Z EPT二级页表 */
    seL4_X86_EPTPDObject,                   /*Z EPT三级页表 */
    seL4_X86_EPTPTObject,                   /*Z EPT四级页表 */
#endif
    seL4_ObjectTypeCount                    /*Z seL4内核对象类型数量 */
} seL4_ArchObjectType;
typedef seL4_Word object_t;

#ifndef CONFIG_IOMMU
#define seL4_X86_IOPageTableObject 0xffffff
#endif

#ifndef CONFIG_VTX
#define seL4_X86_VCPUObject 0xfffffe
#define seL4_X86_EPTPML4Object 0xfffffd
#define seL4_X86_EPTPDPTObject 0xfffffc
#define seL4_X86_EPTPDObject 0xfffffb
#define seL4_X86_EPTPTObject 0xfffffa
#endif

